\section{Przykład} \label{section:przyklad-podstaw}
Przykładowe przejście od twierdzenia zapisanego klasycznie do zapisanego w języku Agda:
\begin{theorem} \label{thm:a-b=0}
    Każde dwie liczby całkowite \(a, b\) dla których \(a - b = 0\) są równe.
  \[ \forall a,b \in \mathbb{Z}: a - b = 0 \implies a = b\]
\end{theorem}
\begin{proof}
  \begin{align*}
    a &= a + 0 && \text{bo $0$ jest elementem neutralnym dodawania} \\
    &= a + (-b + b) && \text{bo $-b$ jest elementem przeciwnym do $b$} \\
    &= (a - b) + b  && \text{bo dodawanie liczb całkowitych jest łączne} \\
    &= 0 + b && \text{z założenia} \\
    &= b && \text{bo $0$ jest elementem neutralnym dodawania}
  \end{align*}
\end{proof}
Poprawność twierdzenia \ref{thm:a-b=0} sprawdza następujący program w języku Agda (składnia Agdy jest opisana w (\ref{sec:podstawy-agdy})):
\begin{code}
  \input{agda-tex/przyklad-liczby-calkowite}
\end{code}
\inlinecode{twierdzenie} jest funkcją przyjmującą trzy argumenty. Pierwsze dwa argumenty (\inlinecode{a} i \inlinecode{b}) to liczby całkowite. Trzeci argument jest dowodem, że różnica pierwszych dwóch argumentów (czyli \inlinecode{a - b}) to \inlinecode{0}. Typ trzeciego argumentu (\inlinecode{założenie}) zależy od wartości pierwszych dwóch argumentów, jest typem zależnym. Wartość zwracana przez funkcję jest dowodem, że pierwsze dwa argumenty są równe (``\texttt{a} $\equiv$ \texttt{b}''). Typ zwracany przez funckję jest typem zależnym.
